米田の補題の証明 ①~②
前提条件などは↑を参照
各$ A,X に対し、$ [\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X) と$ X(A)の間に全単射があることを示す
つまり、$ A,Xを固定して見ている
流れ
そのために
①写像$ [\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)\xrightarrow{(\hat{})} X(A) を定義する
②写像$ [\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)\xleftarrow{(\tilde{})} X(A) を定義する
①②の証明の前の前提のおさらいと目的
$ [\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X) というのは集合である
元は「関手$ H_Aから関手$ Xへ向かう自然変換」である
$ X(A)も集合である
①や②では、この集合間の写像を定義したいわけである
つまり①の場合
https://gyazo.com/53c7f14a5a9876e9709eb649ad984339
$ [\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X) から一つ元(自然変換)$ \alphaを取ってきたときに、
写像の行き先$ \hat{\alpha}を($ \alphaを使って)どう定義するか
が議論の対象になる
②の場合も同様で
https://gyazo.com/4ec6b44378e83d2e9be1b5571807b88e
$ x\in X(A)を取ってきたときに、
写像の行き先である$ \tilde{x}という自然変換を($ xを使って)どう定義するか
が議論の対象になる
①
目的
証明
自然変換$ \alpha:H_A\to Xに対し、
$ \hat\alpha\in Xを、$ \hat\alpha=\alpha_A(1_A)と定義する
補足
図にするとこんなイメージ
https://gyazo.com/66dd1cdba8ecaf3a678fb168d1e8f053
①この自然変換から出発して、
②この中の元に対応させたい
③$ Aの恒等射と、
④$ \alphaの$ A成分に注目すれば、
⑤対応が取れる
簡素すぎてわかりづらいが、他の対応を考えようとしてみても難しいことに気づく
例えば、「じゃあ恒等写像$ 1_A以外のもので対応させてみようや」と思ってやってみるとこうなる
https://gyazo.com/a991ca0723a968973e249dc6956085d6
①恒等射じゃなくて、他の対象$ Bへの射を見てみる
②さっきと同じように対象を取ってくると、、おっとこれは$ X(B)なので、そもそも前提に反する
③気を取り直して、$ X(A)との対応を見ようとするも、この射ってなに？？
②
目的
流れ
$ xに対応する「自然変換$ \tilde{x}:H_A\to Xを定義したい」
コレが目的mrsekut.icon
「...」は自然変換なので、何かしらの射の族である
その射の1つは、$ \tilde{x}_B: \mathscr{A}(B,A)\to X(B)になっているはずである
自然変換の定義から自然に導かれるmrsekut.icon
じゃあ、その$ \tilde{x}_Bを良い感じに定義して、
ここで初めて定義されるmrsekut.icon
このときに、ドメインの$ xを使って良い感じに対応させたい
ここのみが肝であって、これの前後の話はほぼ自明に流れるmrsekut.icon
その族$ \tilde{x}が自然性を満たしていれば、
族の話から自然変換の話に戻ってきているmrsekut.icon
自然性を満たさないと自然変換ではないのでそれを確認する
最初の目的が達成される
証明
$ x\in X(A)についての自然変換$ \tilde{x}:H_A\to Xを定義する
つまり、各$ B\in\mathscr{A}について、
関数$ \tilde{x}_B:H_A(B)=\mathscr{A}(B,A)\to X(B)を定義し、
その族$ \tilde{x}=(\tilde{x}_B)_{B\in\mathscr{A}}が自然性を満たすことを示す
ここで、
$ B\in\mathscr{A}と$ f\in\mathscr{A}(B,A)について、
$ \tilde{x}_B(f)=(Xf)(x)\in X(B)と定義する
これは以下のような対応になる
https://gyazo.com/a9adab08c38182982660fad85ef4a656
同じ$ fから出発して、右回り、左回りで右下に至っているmrsekut.icon
問題はこの経路で来た2つが等しいのかどうかmrsekut.icon
関手$ Xの射の対応より、$ X(f\circ g)=Xg\circ Xfなので、これは等しい
よって上図は可換
補足
どこから$ \tilde{x}_B=(Xf)(x)\in X(B)の定義が来たのか
図にするとこんな感じ
https://gyazo.com/8d30d959252b2c68c675602248d8e617
①ここの$ xから出発して、
②ここに入る対応が欲しい
③そこで元の圏の$ Bとの対応である$ fに着目して
④その対応を見ると、自然に導かれる
この定義を提示されれば「せやな〜」となるけど、思いつけと言われると慣れてないと難しそうmrsekut.icon
書いてる通りだが、自然性を示すために、可換になることを示そうとしている
同じものから出発して、異なる経路で辿ってぶつかった物が等しいことを言えれば
可換である、と言える
これは5項補題の証明でめちゃくちゃ使っているので、良い練習になるmrsekut.icon